perm filename FOUND[1,JRA] blob sn#005818 filedate 1972-10-13 generic text, type T, neo UTF8
00100	xεy⊃S(x);
00200	(S(x)⊃(zεx ≡ zεy))⊃x=y;
00300	S(x) ⊃(∀y(S(y)⊃∃z(S(z)∧∀u(S(u)⊃(uεz ≡(u=x ∨u=y))))));
00400	¬O(x)⊃ ∃y(S(y)∧yεx∧y/x);
00500	O(x) ≡ ∀y(S(y)⊃¬yεx);
00600	x/y ≡ ∀z(S(z) ⊃¬(zεx ∧ zεy)); ;
00700	;
00800	S(x) ⊃ ¬xεx;
00900